The present invention relates to the field of verification of systems.
The systems to which the invention can be applied can be of very diverse kinds. They include in particular sequential or parallel data processing software, communication protocols, control and command systems, distributed systems, electronic components, etc. As a general rule, the invention is applicable to any physical system whose operation can be modelled in the form of communicating automata.
By xe2x80x9cmodelxe2x80x9d is meant an abstraction of the system enabling its operation to be parameterised. In the present instance, it is the translation of the system into the form of automata. The translation must of course preserve the properties of the system as much as possible, whilst allowing flexibility in respect of the verification methods employed.
The term xe2x80x9cautomatonxe2x80x9d means a parametric representation of a part of the system, formed of states and transitions (i.e. of labelled points and arcs) enabling its operation to be described. An automaton can be described in various forms: graphically, textually, in the form of a data processing process, etc. A communicating automaton is an automaton which can exchange information with other automata in the form of sending of messages, synchronisations, etc.
In the context of the present invention, verification consists of demonstrating that the properties of the system as represented by automata are true or false, by exhibiting a path or by proving that a path cannot exist, a path being a succession (obviously a possible succession) of global states of the model. The path gives the ordered sequence of each state of each element of the model. In the present instance, this will be the ordered sequence of states of each automaton constituting the model.
It should be noted that as a general rule the verification is performed on a model and not on the system itself. In this respect it differs from testing, which is more directly related to the finished product. Testing consists of causing the real system to operate (for example the software to execute) to study its behaviour, attempting to cover its operation to the maximum. Many verification workshops enable the real system (the software) to be generated automatically from the model or its specifications to be defined. There is a relatively large number of modelling and verification aid tools (see, for example, A. A. Loureiro et al.: xe2x80x9cFdt tools for protocol developmentxe2x80x9d, in FORTE""92, 1992).
In the field of verification. three types of methods are most often employed:
1. Simulation. Most existing tools enable simulation. It corresponds to running through the states of the model one after the other in accordance with a more or less sophisticated strategy, in order to look for pertinent paths. This method has the advantage that it can be used at any level of abstraction of the system (provided that the abstraction incorporates the path concept) and of being very flexible in use. It has two drawbacks: it runs up against the combinatorial explosion of the number of states of the system (the deeper the search, the greater the number of paths), and it does not prove anything (not finding any path at depth n does not prove that there is none at depth n+1).
2. xe2x80x9cModel-checkingxe2x80x9d (see A. Kerbrat: xe2x80x9cMxc3xa9thodes symboliques pour la vxc3xa9rification de processus communicants: xc3xa9tude et mise en oeuvrexe2x80x9d [xe2x80x9cSymbolic methods for verifying communicating processes: design and implementationxe2x80x9d], PhD thesis, University Joseph Fourier, Grenoble, 1994, or K. L. McMillan: xe2x80x9cSymbolic Model Checkingxe2x80x9d, Kluwer Academic Publishers, 1993). xe2x80x9cModel-checkingxe2x80x9d methods require modelling of the system in the form of automata. The automata of such modelling are fused into a single automaton in which each state corresponds to a global state of the model. It is then possible to verify properties described in temporal logic on the global automaton. The advantage of this method lies in the richness of the temporal software, which enables a very large number of types of requests to be specified. It also facilitates simulation. However, it has the limitation of very quickly generating a global automat of gigantic size which as a general rule can therefore not be constructed, despite a number of techniques for reducing the size of the automaton (use of global automaton coding techniques, fabrication of a model of the global automaton with weaker properties, etc.).
3. Proof by theorems (see J.-R. Abrial: xe2x80x9cThe B-bookxe2x80x9d, Cambridge University Press, 1995, or B. Chetali: xe2x80x9cFormal verification of concurrent programs: How to specify UNITY using the Larch Proverxe2x80x9d, Technical report, INRIA, France, 1995). Here the model consists of a set of logic formulae which describe its basic properties. A new property to be verified being given in the form of a logical formula, a proof will consist of successive steps enabling the new logic formula to be obtained from logical formulae of the model and inference rules. This method has the advantage of producing true formal proofs. However, there are no good inference strategies at present and the computer is almost always reduced merely to solving the simple steps of the proof and leaving the hard parts to the human logicist.
In the field of Petri networks, it is known in the art to use optimisation methods employing linear programming to verify systems. However, linear programming is used only on very highly constrained models which therefore cannot be used to model real systems (see J. Esparza et al.: xe2x80x9cA polynomial-time algorithm to decide liveness of bounded free choice netsxe2x80x9d, Theoretical Computer Science, 102: 185-205, 1992), or to generate the set of invariants of the model studied (in particular the Fourier-Motzkin algorithm), which set is constructed without discernment and rapidly becomes of gigantic size.
More recently, the direct use of integer programming on a communicating automata model has been studied (see J. C. Corbett: xe2x80x9cAutomated Formal Analysis Methods for Concurrent and Real-Time Softwarexe2x80x9d, PhD thesis, Department of Computer Science, University of Massachusetts, USA, 1992). However, using integer programming does not provide sufficient algorithms and most importantly cannot perform proofs on the model. This research team studied the power of expressivity of the request system in depth and deduced that it was very close to temporal logic.
Another use of linear programming in the field of verification is described by J. L. Lambert (xe2x80x9cPrxc3xa9sentation du projet validation de protocoles par programmation linxc3xa9airexe2x80x9d [xe2x80x9cDescription of the protocol validation by linear programming projectxe2x80x9d], Technical Report 27, Greyc, University of Caen, 1994). This approach does not involve any concept of ordering messages, which constitutes a limitation on the operating conditions of the system which can be analysed.
The object of the present invention is to enrich verification techniques by proposing a method that is capable of proving properties of the system studied and whose complexity does not increase too dramatically with the size of the system.
The invention therefore proposes a method of verifying the operation of a system modelled by a system of automata synchronised by a set of messages, including the following operations:
breaking down the system into N subsystems numbered from n=1 to n=N;
providing parameters describing each subsystem n (1xe2x89xa6nxe2x89xa6N) in the form of a respective automaton composed of a set En of states eni of the subsystem n with a set An of transitions anj between pairs of states of the set En, each transition a of the set Anj being associated with a subset Mnj of the set of synchronisation messages to translate the fact that each message of the subset Mnj arises when the subsystem described changes state in accordance with the transition anj;
constructing a system of linear equations including, for 1xe2x89xa6txe2x89xa6T and 1xe2x89xa6nxe2x89xa6N, on the one hand flow equations of the form:             e      n      i        ⁢          xe2x80x83        ⁢          (              t        -        1            )        =                    ∑                  j          ∈                      B            n            i                              ⁢              xe2x80x83            ⁢                        a          n          j                ⁢                  xe2x80x83                ⁢                  (          t          )                ⁢                  xe2x80x83                ⁢        for        ⁢                  xe2x80x83                ⁢                  e          n          i                      ∈          E      n      
xe2x80x83and of the form:                     e        n        i            ⁢              xe2x80x83            ⁢              (        t        )              =                            ∑                      j            ∈                          C              n              i                                      ⁢                  xe2x80x83                ⁢                              a            n            j                    ⁢                      xe2x80x83                    ⁢                      (            t            )                    ⁢                      xe2x80x83                    ⁢          for          ⁢                      xe2x80x83                    ⁢                      e            n            i                              ∈              E        n              ,
xe2x80x83and on the other hand synchronisation equations of the form.                     m        k            ⁢              xe2x80x83            ⁢              (        t        )              =                            ∑                      j            ∈                          D              n              k                                      ⁢                  xe2x80x83                ⁢                              a            n            j                    ⁢                      xe2x80x83                    ⁢                      (            t            )                    ⁢                      xe2x80x83                    ⁢          for          ⁢                      xe2x80x83                    ⁢                      m            k                              ∈              M        n              ,
xe2x80x83where T designates a number of successive steps of the operation of the system, Bni designates the set of the indices j such that the transition anj of the set An starts from the state eni of the set En, Cni designates the set of the indices j such that the transition anj of the set An leads to the state eni of the set En, Mn designates the union of the subsets of messages Mnj respectively associated with the transitions of the set An, Dnk designates the set of the indices j such that a message mk of the set Mn belongs to the subset Mnj associated with the transition anj of the set An, the variable eni (t) (0xe2x89xa6txe2x89xa6T) is an unknown of the linear system associated with the state eni of the set En and with step t, the variable anj(t) (1xe2x89xa6txe2x89xa6T) is an unknown of the linear system associated with the transition anj of the set An and with step t, the variable mk(t) (1xe2x89xa6txe2x89xa6T) is an unknown of the linear system associated with the message mk of the set of synchronisation messages and with step t;
defining a property of the system to be verified in the form of additional linear constraints imposed on the unknowns of the linear system;
applying a linear programming solution method to the linear system subject to the additional constraints;
analysing the result of linear programming to determine if said property is verified by the system; and
assisting a user to detect malfunction of said system or to obtain evidence of correct operation of said system.
This method has few points in common with the three prior art methods commented on above. Like xe2x80x9cmodel-checkingxe2x80x9d, it is based on modelling in the form of communicating automata but the comparison stops there. The system of requests is of the same order of expressivity as temporal logic, although it is closer to the path concept than the latter: in the present instance, requests are typically based on questions of accessibility of states and transitions and sending or receiving messages. A fundamental difference compared to xe2x80x9cmodel-checkingxe2x80x9d is that the method operates directly on the automata of the model without using a global automaton produced from all the automata of the model. Also, the proofs given by linear programming correspond to sums of equations which can yield an equation that is trivially false. They are therefore unrelated to proof by theorems. The method can also furnish paths validating a request. However, this path is constructed directly, without running through these states, as simulation or model-checking would. The solution proposed by linear programming is not necessarily an integer value path. It is therefore necessary to construct a model of automata which minimises the number of non-integer solutions and which enables them to be interpreted and eliminated when they occur, by introducing pertinent additional linear constraints.